\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Config}$:AbsInterface(chain\_config()), ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)),\+
\\[0ex]$e$:E.
\-\\[0ex]($\uparrow$($e$ $\in_{b}$ ${\it Sys}$(valid))) $\Leftarrow\!\Rightarrow$ (($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) \& valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$e$))
\end{tabbing}